Nuprl Lemma : symmetrize_wf
12,41
postcript
pdf
T
:Type{j},
R
:(
T
T
{i}),
a
,
b
:
T
. Symmetrize(
x
,
y
.
R
(
x
,
y
);
a
;
b
)
{i}
latex
ProofTree
Definitions
P
&
Q
,
x
(
s1
,
s2
)
,
Symmetrize(
x
,
y
.
R
(
x
;
y
);
a
;
b
)
,
t
T
,
,
x
:
A
.
B
(
x
)
origin
T:Type{j}, R:(T
T
{i}), a, b:T. Symmetrize(x,y.R(x,y);a;b) 
{i}
T:Type{j}, R:(TT{i}), a, b:T. Symmetrize(x,y.R(x,y);a;b) {i}
Tx:A. B(x)